;; Copyright © 2016, cage
;; All rights reserved.

;; Redistribution and use in source and binary forms, with or without
;; modification, are permitted provided that the following conditions are met:

;;     * Redistributions of source code must retain the above copyright
;; notice, this list of conditions and the following disclaimer.
;;     * Redistributions in binary form must reproduce the above copyright
;; notice, this list of conditions and the following disclaimer in the
;; documentation and/or other materials provided with the distribution.

;; THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
;; AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
;; IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
;; ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
;; LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
;; CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
;; SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
;; INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
;; CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
;; ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF
;; THE POSSIBILITY OF SUCH DAMAGE.

(in-package :interface)

(defmethod equivp (lhs rhs)
  (eql lhs rhs))

(defmethod equivp ((lhs mu-var) (rhs mu-var))
  (mu-var= lhs rhs))

(defmethod equivp ((lhs string) (rhs string))
  (string= lhs rhs))

(defmethod equivp ((lhs vector) (rhs vector))
  (or (eq lhs rhs)
      (and (eql (length lhs) (length rhs))
	   (progn (map nil (lambda (l r)
			     (unless (equivp l r)
			       (return-from equivp +failed-unification+)))
		       lhs rhs)
		  t))))

(defmethod equivp ((lhs list) (rhs list))
  (or (eq lhs rhs)
      (and lhs rhs
	   (equivp (car lhs) (car rhs))
	   (equivp (cdr lhs) (cdr rhs)))))

(defmethod unify-impl (u v subst)
  (if (equivp u v)
      subst
      +failed-unification+))

(defmethod unify-impl ((u mu-var) (v mu-var) subst)
   (if (equivp u v)
       subst
       (call-next-method)))

(defmethod unify-impl ((u mu-var) v subst)
  (extend-subst u v subst))

(defmethod unify-impl (u (v mu-var) subst)
  (extend-subst v u subst))

(defmethod unify-impl ((u cons) (v cons) subst)
  (let ((subst-2 (unify (car u) (car v) subst)))
    (if (not (failed-unification-p subst-2))
	(unify (cdr u) (cdr v) subst-2)
	+failed-unification+)))

(defmethod unify-impl ((u vector) (v vector) subst)
  (let ((len (length u)))
    (cond ((= len (length v))
	   (map nil (lambda (u v)
		      (setf subst (unify u v subst))
		      (when (failed-unification-p subst)
			(return-from unify-impl +failed-unification+)))
		u v)
	   subst)
	  (t +failed-unification+))))

(defgeneric walk-impl (val subst)
  (:method (val subst)
    (declare (ignore subst))
    val)
  (:method ((val string) subst)
    (declare (ignore subst))
    val)
  (:method ((val cons) subst)
    (cons (walk* (car val) subst)
          (walk* (cdr val) subst)))
  (:method ((val vector) subst)
    (map (type-of val)
         (lambda (val)
           (walk* val subst))
         val)))

(defgeneric reify-subst-impl (val subst)
  (:method (val subst)
    (declare (ignore val))
    subst)
  (:method ((val string) subst)
    (declare (ignore val))
    subst)
  (:method ((val mu-var) subst)
    (extend-subst val (reify-name (length subst)) subst))
  (:method ((val cons) subst)
    (reify-subst (cdr val) (reify-subst (car val) subst)))
  (:method ((val vector) subst)
    (reduce (lambda (subst item)
              (reify-subst item subst))
            val
            :initial-value subst)))

(defgeneric reify-name (n))

(defmethod reify-name ((n number))
  (intern (format nil "_.~a" n) :keyword))

;; not strictly part  of the interfaces but i have  not found a better
;; place for these

(defun reify-subst (id? subst)
  (let ((id? (walk id? subst)))
    (reify-subst-impl id? subst)))

(defun walk* (id? subst)
  (let ((id? (walk id? subst)))
    (walk-impl id? subst)))
